package ca.shojaei.mini_sat;

import java.util.*;

public class ForAllUntil extends Clause {
	
	public ForAllUntil() {
		super();
		this.unary = false;
		this.evaluable = true;
	}
	private Clause F;
	private Clause G;
	private String symbol = "aU";
	public ForAllUntil(Clause f, Clause g, String symbol) {
		super();
		F = f;
		G = g;
		this.symbol = symbol;
		this.unary = false;
	}
	public Clause getLeft(){
		return getF();
	}
	public void setLeft(Clause c){
		setF(c);
	}
	
	public Clause getRight(){
		return getG();
	}
	public void setRight( Clause c){
		setG(c);
	}
	
	public Clause getF() {
		return F;
	}
	public void setF(Clause f) {
		F = f;
	}
	public Clause getG() {
		return G;
	}
	public void setG(Clause g) {
		G = g;
	}
	public String getSymbol() {
		if(this.negated){
			String str = "!".concat(this.symbol);
			return str;
		}
		return symbol;
	}
	public void setSymbol(String symbol) {
		this.symbol = symbol;
	}
	@Override
	public Vector<int[]> getDIMACS(Model m) {
		// TODO Auto-generated method stub
		return null;
	}
	@Override
	public boolean evaluate(Model m) {
		
		boolean out = true;
        State cur = m.getCurrentStat();
		m.reSetVisit();
		if(G.evaluate(m))
		{
			if(negated) return false;
			return true;
		}
		if(F.evaluate(m))
		{
		
			m.getCurrentStat().setVisited(true);
			Vector<State> nexts = m.getCurrentStat().getNexts();
			
			for(int i = 0 ; i < nexts.size(); i++)
			{
				if(nexts.get(i).getStateName() == m.getCurrentStateName())
				{
					if(nexts.size() > 1) continue;
				}
				m.setCurrentStat(nexts.get(i).getStateName());
				
				if(!until(m, F, G )){
					
					out = false;
					break;
				}
			}
			
			// Set the current state back to what it was
			m.setCurrentStat(cur.getStateName());
			if(negated) out = !out;
			return out;
			
		}else{
			if(negated) return true;
			return false;
		}
    		
	}
	private boolean until(Model m, Clause F, Clause G){
		
		boolean out = true;
		State cur = m.getCurrentStat();
		if(G.evaluate(m ))
			return true;
		if(m.getCurrentStat().isVisited())
		{
			return false;
		}
		
		
		if(F.evaluate(m))
		{
			Vector<State> nexts = m.getCurrentStat().getNexts();
			
			for(int i = 0 ; i < nexts.size(); i++)
			{
				
				State temp = nexts.get(i);
				if(m.getCurrentStateName() == temp.getStateName())
				{
					if(nexts.size() > 1 )
					
					continue;
				}
				m.getCurrentStat().setVisited(true);
				m.setCurrentStat(nexts.get(i).getStateName());
				
				if(!until(m, F, G )){
					
					out = false;
					break;
				}
				
				
				// Set the current state back to what it was
				m.setCurrentStat(cur.getStateName());
				
			}
			
			
			return out;
			
		}else{
			return false;
		}
		
	}
	
}
